Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    x - 0  → x
2:    s(x) - s(y)  → x - y
3:    p(s(x))  → x
4:    f(s(x),y)  → f(p(s(x) - y),p(y - s(x)))
5:    f(x,s(y))  → f(p(x - s(y)),p(s(y) - x))
There are 11 dependency pairs:
6:    s(x) -# s(y)  → x -# y
7:    F(s(x),y)  → F(p(s(x) - y),p(y - s(x)))
8:    F(s(x),y)  → P(s(x) - y)
9:    F(s(x),y)  → s(x) -# y
10:    F(s(x),y)  → P(y - s(x))
11:    F(s(x),y)  → y -# s(x)
12:    F(x,s(y))  → F(p(x - s(y)),p(s(y) - x))
13:    F(x,s(y))  → P(x - s(y))
14:    F(x,s(y))  → x -# s(y)
15:    F(x,s(y))  → P(s(y) - x)
16:    F(x,s(y))  → s(y) -# x
The approximated dependency graph contains 2 SCCs: {6} and {7,12}.
Tyrolean Termination Tool  (0.03 seconds)   ---  May 3, 2006